-
Notifications
You must be signed in to change notification settings - Fork 105
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
More monad improvements #765
Conversation
b68c9eb
to
ac32aed
Compare
There are two new commits in this PR, which removes one lemma from Nondet_VCG, along with removing some FIXMEs that I had recently added and which I no longer think are worth doing. I do still think that the lemmas the FIXMEs refer to are a bit unnecessary, but they're already used in enough proofs that they might as well be left in, and probably should even have their equivalents added to I removed |
| simp add: projectKO_opt_tcb projectKO_opt_cte | ||
makeObject_cte makeObject_tcb archObjSize_def | ||
tcb_cte_cases_def objBitsKO_def APIType_capBits_def | ||
objBits_def createObjects_def bit_simps | ||
| intro conjI impI | ||
| fastforce simp: curDomain_def)+ | ||
| clarsimp simp: curDomain_def)+ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this a consequence of removing hoare_gets
, or was fastforce more powerful than was needed in general? I've noticed a few instances of that in this commit.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's a consequence of removing hoare_gets
. Roughly, this proof previously used wp
until it hit curDomain
, which the fastforce
would unfold and then solve using hoare_gets
as an intro
rule. Now, the clarsimp
is just being used to do the unfold and then it goes back to wp
to solve the goal. I don't remember exactly why, but for some reason I thought that the unfold couldn't happen ahead of time.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looking at it again here, the clarsimp
and simp
could probably be combined though.
apply (clarsimp simp: validE_E_def) | ||
by (wp | assumption)+ | ||
|
||
lemmas bind_wp_fwd = bind_wp[rotated] | ||
lemmas bindE_wp_fwd = bindE_wp[rotated] | ||
|
||
lemma bind_wpE_R: | ||
"\<lbrakk>\<And>x. \<lbrace>Q' x\<rbrace> g x \<lbrace>Q\<rbrace>,-; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,-" | ||
"\<lbrakk>\<And>rv. \<lbrace>Q' rv\<rbrace> g rv \<lbrace>Q\<rbrace>,-; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= (\<lambda>rv. g rv) \<lbrace>Q\<rbrace>,-" |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
good, I'm glad you remember the significance of the etas
done | ||
"\<lbrakk> P \<or> P'; P \<Longrightarrow> \<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>; P' \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> | ||
\<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> S s) \<and> (P' \<longrightarrow> T s)\<rbrace> f \<lbrace>Q\<rbrace>" | ||
by (fastforce intro: hoare_weaken_pre) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
hahaha wow
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I want to say a huge thanks for your recent crusade to reduce the jankiness of our proofs.
Feedback:
commits:
- is it worth having three commits for updating the proofs after the monad consistency commit? I'd squash at least the automated ones together, and maybe even the manual one.
- keeping the remove FIXMES ones separate is a good idea
commit messages:
- apart from hoare_gets -> apart from removing hoare_gets
questions:
- what the
-0777
argument toperl
do?
I'm happy to squash the automated ones together, I think I mostly did it this way due to starting off with the easy lemma renames and then gradually working out what was needed to change the variables. I wouldn't mind keeping the manual one separate though, I expect it to help when merging into
Agreed, the only one I'm not sure about is the FIXME that was added in the first commit of this PR.
👍
I have to admit that this is a command I dug up from the last time I used |
Agreed, let's squash the automated ones and keep the manual fix-up so we can transfer it. The gitlint check fails because the regular expressions in the commit message are too long. I think I'd be fine overriding the check for this instance. @Xaphiosis do you agree? |
Thanks, one more step towards sanity! :-) |
ce27e67
to
fe38d0f
Compare
This makes the lemma names in the monad rule sets even more consistent, and changes the variables used in the lemmas to avoid R and G being used in pre or post-conditions. These variable names are instead reserved for the rely and guarantee conditions in the trace monads RG rule set. Signed-off-by: Corey Lewis <[email protected]>
The following commands are updates for changed lemma names: sed -i 's/hoare_valid_validE/valid_validE/g' **/*.thy sed -i 's/hoare_vcg_E_conj/hoare_vcg_conj_liftE_E/g' **/*.thy sed -i "s/hoare_vcg_conj_liftE_R/hoare_vcg_conj_liftE_R'/g" **/*.thy sed -i 's/hoare_vcg_R_conj/hoare_vcg_conj_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_E_elim/hoare_vcg_conj_elimE/g' **/*.thy sed -i 's/hoare_vcg_const_imp_lift_R/hoare_vcg_const_imp_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_const_Ball_lift_R/hoare_vcg_const_Ball_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_conj_lift_R/hoare_vcg_conj_liftE_R/g' **/*.thy sed -i 's/hoare_vcg_const_imp_lift_E/hoare_vcg_const_imp_liftE_E/g' **/*.thy sed -i 's/hoare_weak_lift_imp_R/hoare_weak_lift_impE_R/g' **/*.thy sed -i 's/hoare_post_imp_dc2_actual/hoare_post_impE_R_dc_actual/g' **/*.thy sed -i 's/hoare_post_imp_dc2E_actual/hoare_post_impE_E_dc_actual/g' **/*.thy sed -i 's/hoare_post_imp_dc2E/hoare_post_impE_E_dc/g' **/*.thy perl -0777 -pi -e 's/hoare_pre\(1\)/hoare_weaken_pre/g' **/*.thy perl -0777 -pi -e 's/hoare_drop_imps\(2\)/hoare_drop_impE_R/g' **/*.thy sed -i 's/hoare_vcg_imp_lift_R/hoare_vcg_imp_liftE_R/g' **/*.thy The following commmands update changed variable names: perl -0777 -pi -e "s/hoare_post_imp\h*(\s*)\[(\s*)where\h*Q\h*=\h*/hoare_post_imp\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_post_imp/rule_tac Q'=\"\1\"\2in hoare_post_imp/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_strengthen_post/rule_tac Q'=\"\1\"\2in hoare_strengthen_post/g" **/*.thy perl -0777 -pi -e "s/hoare_strengthen_post\h*(\s*)\[(\s*)where\h*Q\h*=\h*/hoare_strengthen_post\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_strengthen_post\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_strengthen_post\1\[\2where Q=/g" **/*.thy perl -0777 -pi -e "s/hoare_drop_impE_R\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_drop_impE_R\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_drop_imp\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_drop_imp\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_drop_imps\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_drop_imps\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*G\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_grab_asm/rule_tac P'=\"\1\"\2in hoare_grab_asm/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*R\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_vcg_if_split/rule_tac P''=\"\1\"\2in hoare_vcg_if_split/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*R\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_post_add/rule_tac Q'=\"\1\"\2in hoare_post_add/g" **/*.thy perl -0777 -pi -e "s/hoare_strengthen_postE\h*(\s*)\[where\h*E\h*=\h*/hoare_strengthen_postE\1\[\2where E'=/g" **/*.thy perl -0777 -pi -e "s/hoare_disjI2\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_disjI2\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_weaken_pre/rule_tac P'=\"\1\"\2in hoare_weaken_pre/g" **/*.thy perl -0777 -pi -e "s/hoare_weaken_pre\h*(\s*)\[(\s*)where\h*Q\h*=\h*/hoare_weaken_pre\1\[\2where P'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_pre_imp/rule_tac P'=\"\1\"\2in hoare_pre_imp/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)and(\s*)E\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_strengthen_postE/rule_tac Q'=\"\1\"\2and\3E'=\"\4\"\5in hoare_strengthen_postE/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*E\h*=\h*\"([^\"]+)\"(\s*)and(\s*)Q\h*=\h*\"([^\"]+)\"(\s*)in\h*hoare_strengthen_postE/rule_tac E'=\"\1\"\2and\3Q'=\"\4\"\5in hoare_strengthen_postE/g" **/*.thy perl -0777 -pi -e "s/hoare_vcg_conj_liftE_R\h*(\s*)\[(\s*)where\h*S\h*=\h*/hoare_vcg_conj_liftE_R\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/hoare_post_add\h*(\s*)\[(\s*)where\h*R\h*=\h*/hoare_post_add\1\[\2where Q'=/g" **/*.thy perl -0777 -pi -e "s/rule_tac\h*Q\h*=\h*\"([^\"]+)\"(\s*)for(.*)(\s*)in\h*hoare_strengthen_post/rule_tac Q'=\"\1\"\2for\3\4in hoare_strengthen_post/g" **/*.thy perl -0777 -pi -e "s/unless_wp\h*(\s*)\[(\s*)where\h*Q\h*=\h*/unless_wp\1\[\2where P'=/g" **/*.thy perl -0777 -pi -e "s/hoare_chain\h*(\s*)\[(\s*)where\h*P\h*=\h*/hoare_chain\1\[\2where P'=/g" **/*.thy Signed-off-by: Corey Lewis <[email protected]>
This fixes the proofs not handled by the automated changes in the previous commits. Signed-off-by: Corey Lewis <[email protected]>
These FIXMEs were recently added and apart from removing hoare_gets I no longer think that they are worth doing, as the lemmas they refer to are used in more proofs than I first thought. Signed-off-by: Corey Lewis <[email protected]>
Signed-off-by: Corey Lewis <[email protected]>
fe38d0f
to
f69d902
Compare
This makes further improvements to the consistency of the monad rule sets, following on from #759. In particular, it includes additional lemma renamings missed in that PR, and changes the variables used in the lemmas to avoid
R
andG
being used in pre or post-conditions. These variable names are instead reserved for the rely and guarantee conditions in the trace monad's RG rule set.